T:Type, L:(T List). fseg(T;L;[])  (null(L)) 

latex

ProofTree

Definitions

s = t, type List, f(a), as @ bs, [], rec-case(a) of [] => s | x::y => z.t(x;y;z), [car / cdr], s ~ t, ||as||, b, A, null(as), p =b q, i <z j, i z j, (i = j), x =a y, a < b, x f y, a < b, [d], b, p  q, p  q, p q, Type, x.A(x), Y, x:A. B(x), x:A. B(x), P  Q, fseg(T;L1;L2), x:A  B(x), P & Q, x:AB(x), P  Q, P  Q, left + right, P  Q, Dec(P), b | a, a ~ b, a  b, a <p b, a < b, A c B, xL. P(x), (xL.P(x)), False, t  T, True, , tt, Void, #$n, , T,

Lemmas

append wf, assert of null, iff wf, not wf, bool wf, null wf, squash wf, true wf, btrue wf, decidable assert, rev implies wf, assert wf